(defprop simpl (
 SIMPLIFY
 SIMPL
 APPLY_RULE
 MATCHSUBST
 FIND_MATCH
 FIND→
 CMATCH
 INST
 ISVAR
 REQUEST
 PRINT_MATCH
 SUBSTFREE
 ISDEF
) simplfns)


;;; Top level for simplifying an expression according to a set of rules

(DEFUN SIMPLIFY ()
  (PROG (RULES PRINT&MATCH)
  GET_RULES
    (SETQ RULES (GET (REQUEST '|Name of rules: |) 'RULE))
  GET_EXP
    (SETQ PRINT&MATCH (REQUEST  '|Do you wish matches printed out (t or nil)?  |))
    (PRINT (SIMPL (REQUEST '|Expression to simplify:  |)) )
    (COND ((NOT (REQUEST '|Do you wish to do more (t or nil)?  |)) (RETURN 'SO-LONG)) )
    (COND ((REQUEST '|Do you wish to specify new rules (t or nil)?  |) 
	   (GO GET_RULES)) )
    (GO GET_EXP)
  ))

;;; SIMPL SEARCHES FOR A RULE TO APPLY AND DOES THE CORRESPONDING ACTION
;;; ITERATIVE VERSION WOULD BE BETTER

(DEFUN SIMPL (EXP)
  ((LAMBDA (M) 
      (COND ((NULL M) EXP) 
	    (T (COND (PRINT&MATCH (PRINT_MATCH EXP M)) )
	       (SIMPL (APPLY 'APPLY_RULE M))) ))
   (FIND_MATCH EXP RULES) ))

;;;APPLY_RULE(MATCHLIST,FLAG,RESULT) REPLACES ALL THE VARS IN MATCHLIST BY THEIR
;;;	ASSOCIATED VALUES AND RETURNS RESULT IF FLAG=NIL OR (EVAL RESULT) OW

(DEFUN APPLY_RULE (MATCHLIST ACTION FLAG)
 (COND (FLAG (EVAL (MATCHSUBST ACTION MATCHLIST)))
	(T (MATCHSUBST ACTION MATCHLIST)) ))

(DEFUN MATCHSUBST (EXP ML)
  (COND ((ATOM EXP) ((LAMBDA (Z) (COND ((NULL Z) EXP) (T (CDR Z)) )) (ASSOC EXP ML)) )
	(T (CONS (MATCHSUBST (CAR EXP) ML) (MATCHSUBST (CDR EXP) ML))) ))


;;; MATCH ONE LEVEL SIMPLE MATCH ASSIGNS THINGS TO VARS IF SORTS ARE COMPATIBLE
;;;     AND RETURNS AN ASSOC LIST OR THE ATOM 'NOMATCH

(DEFUN FIND_MATCH (EXP RULES)
  (COND ((NULL RULES) NIL) 
        (T ((LAMBDA (M) (COND ((EQ M 'NOMATCH) (FIND_MATCH EXP (CDR RULES)))
			      (T (CONS M (FIND→ (CAR RULES)))) ))
	    (CMATCH EXP 
		  (CAAR RULES) 
		  (COND ((EQ (CADAR RULES) '→) T) (T (CADAR RULES))) )) ) ))

(DEFUN FIND→ (U)
  (COND ((NULL U) (LIST 'ERROR&RULE NIL))
	((EQ (CAR U) '→) (CDR U) )
	(T (FIND→ (CDR U))) ))

;;; conditional match of pattern containing variables to an expression
;;; matching variables values must satisfy the test.

(DEFUN CMATCH (EXP PAT TEST)
  ((LAMBDA (ML) 
    (COND ((EQ ML 'NOMATCH) ML) 
	  ((EVAL (MATCHSUBST TEST ML)) ML) 
	  (T 'NOMATCH))) 
   (INST EXP PAT NIL)) )

(DEFUN INST (E PAT ML) 
  (COND ((EQ ML (QUOTE NOMATCH)) ML) 
	((ATOM PAT) 
	  (COND ((ISVAR PAT)
		  ((LAMBDA (W) (COND ((NULL W) (CONS (CONS PAT E) ML))
				     ((EQUAL (CDR W) E) ML) 
				     (T (QUOTE NOMATCH)))) 
		   (ASSOC PAT ML)))
		((EQ PAT E) ML) 
		(T (QUOTE NOMATCH)))) 
	((ATOM E) (QUOTE NOMATCH))
	(T (INST (CDR E) (CDR PAT) (INST (CAR E) (CAR PAT) ML)))))

(DEFUN ISVAR (PAT) 
  ((LAMBDA (X) (AND (EQ (CAR X) '&) (NOT (NULL (CDR X) ))))
   (EXPLODEC PAT))
)

(DEFUN REQUEST (MSG) (TERPRI) (PRINC MSG) (READ))

(DEFUN PRINT_MATCH (EXP M)
  (PROG NIL
    (TERPRI) (PRINC '|Expression being matched: |) (PRINC EXP)
    (TERPRI) (PRINC '|Bindings: |) (PRINC (CAR M))
    (TERPRI) (PRINC '|Action: |) (PRINC (CADR M)) (TERPRI) ))

(DEFUN SUBSTFREE (VAL VAR EXP)
  (COND ((ATOM EXP) (COND ((EQ VAR EXP) VAL) (T EXP)))
	((EQ (CAR EXP) 'QUOTE) EXP)
	((EQ (CAR EXP) 'COND) 
	  (CONS 'COND 
		(MAPCAR (FUNCTION (LAMBDA (X) (LIST (SUBSTFREE VAL VAR (CAR X))
						    (SUBSTFREE VAL VAR (CADR X)))))
			(CDR EXP))))
	((ATOM (CAR EXP)) 
	  (CONS (CAR EXP) 
		(MAPCAR (FUNCTION (LAMBDA (X) (SUBSTFREE VAL VAR X))) (CDR EXP))))
	((EQ (CAAR EXP) 'LAMBDA) 
	  (CONS (LIST (CAAR EXP) 
		      (CADAR EXP) 
		      (COND ((MEMBER VAR (CADAR EXP)) (CADDAR EXP))
			    (T (SUBSTFREE VAL VAR (CADDAR EXP)))))
		(MAPCAR (FUNCTION (LAMBDA (X) (SUBSTFREE VAL VAR X))) (CDR EXP))))
	(T 'ERROR&SUBSTFREE) ))

(DEFUN ISDEF (F) (NOT (NULL (GET F 'EXPR))))
;;; Sample set of rules for interpreting LISP terms

(PROG NIL

(PUTPROP 'LISP 
'(
(T → (QUOTE T) NIL)
(NIL → (QUOTE NIL) NIL)
(&N  (NUMBERP '&N)  → (QUOTE &N) NIL)
((COND (&X1 &X2) . &Y)  →  
	(CONS '& (CONS 'COND (CONS (LIST (SIMPL '&X1) '&X2)  '&Y))) T)
((& COND ((QUOTE T) &X2) . &Y)  →  &X2  NIL)
((& COND ((QUOTE NIL) &X2) . &Y)  →  (COND . &Y) NIL)
((COND) → ERROR&COND NIL)
((AND &X . &Y) → (CONS '& (CONS 'AND (CONS (SIMPL '&X)  '&Y))) T)
((AND) → (QUOTE T) NIL)
((& AND (QUOTE T) . &Y) → (AND . &Y) NIL)
((& AND (QUOTE NIL) . &Y) → (QUOTE NIL) NIL)
((OR &X . &Y) → (CONS '& (CONS 'OR (CONS (SIMPL '&X)  '&Y))) T)
((OR) → (QUOTE NIL) NIL)
((& OR (QUOTE NIL) . &Y) → (OR . &Y) NIL)
((& OR (QUOTE T) . &Y) → (QUOTE T) NIL)
((NOT &X) → (CONS '& (CONS 'NOT (SIMPL '&X))) T)
((& NOT (QUOTE T)) → (QUOTE NIL) NIL)
((& NOT (QUOTE NIL)) → (QUOTE T) NIL)
((CAR &X) → (LIST '& 'CAR (SIMPL '&X)) T)
((& CAR (QUOTE &X)) →  (LIST 'QUOTE (CAR (QUOTE &X))) T)
((CDR &X) → (LIST '& 'CDR (SIMPL '&X)) T)
((& CDR (QUOTE &X)) →  (LIST 'QUOTE (CDR (QUOTE &X))) T)
((ATOM &X) → (LIST '& 'ATOM (SIMPL '&X)) T)
((& ATOM (QUOTE &X)) →  (LIST 'QUOTE (ATOM (QUOTE &X))) T)
((NULL &X) → (LIST '& 'NULL (SIMPL '&X)) T)
((& NULL (QUOTE &X)) →  (LIST 'QUOTE (NULL (QUOTE &X))) T)
((CONS &X &Y) → (LIST '& 'CONS (SIMPL '&X)(SIMPL '&Y)) T)
((& CONS (QUOTE &X) (QUOTE &Y)) →  (LIST 'QUOTE (CONS (QUOTE &X) (QUOTE &Y))) T)
((EQ &X &Y) → (LIST '& 'EQ (SIMPL '&X)(SIMPL '&Y)) T)
((& EQ (QUOTE &X) (QUOTE &Y)) →  (LIST 'QUOTE (EQ (QUOTE &X) (QUOTE &Y))) T)

( ((LAMBDA . &Y) &X . &Z)  →
	(CONS (CONS '& (CONS 'LAMBDA  '&Y)) (CONS (SIMPL '&X) '&Z)) T)

( ((& LAMBDA (&V.&X) &Y) (QUOTE &V1) . &Z)  (ATOM '&V) →
	(CONS (LIST 'LAMBDA '&X (SUBSTFREE  '(QUOTE &V1) '&V '&Y)) '&Z) T)
( ((LAMBDA NIL &Y))  → &Y NIL)
((&F . &Y)  (ISDEF '&F) → (CONS (GET '&F 'EXPR) '&Y) T)
)
'RULE)
(RETURN 'LISP&RULE))
;;; Sample runs

;;;Expression to simplify:  T
;;;(QUOTE T) 
;;;Expression being matched: (AND (COND (NIL NIL) (T T)) T)
;;;(QUOTE T) 
;;;Expression being matched: ((LAMBDA (X) X) (CDR (QUOTE (A . B))))
;;;(QUOTE B) 
;;;Expression being matched: (LEFT (QUOTE (C . D)))
;;;(QUOTE C)